($\lambda$$A$,${\it op}$,${\it id}$,$p$,$q$,$E$,$z$. $\Pi$(${\it op}$,${\it id}$) $p$ $\leq$ $i$ $<$ $q$. $E$($i$))
\\[0ex]$\in$ $A$:Type$\rightarrow$($A$$\rightarrow$$A$$\rightarrow$$A$)$\rightarrow$$A$$\rightarrow$($p$,$q$:$\mathbb{Z}\rightarrow$(\{$p$..$q$$^{-}$\}$\rightarrow$$A$)$\rightarrow$($\downarrow$True)$\rightarrow$$A$)